Programmable logic controllers (PLCs) are special embedded computers that are widely\nused in industrial control systems. To ensure the safety of industrial control systems, it is necessary\nto verify the correctness of PLCs. Formal verification is considered to be an effective method\nto verify whether a PLC program conforms to its specifications, but the expertise requirements\nand the complexity make it hard to be mastered and widely applied. In this paper, we present a\nspecification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires\nusers to review specifications mined from the program behaviors instead of model checking for\nspecified specifications, which can greatly improve the efficiency of safety verification and is\nmuch easier for control system engineers to use. Moreover, we implement a proof-of-concept\ntool named PLCInspector that supports directly mining LTL specifications and data invariants from\nPLC programs. Two examples and one real-life case study are presented to illustrate its practicability\nand efficiency. In addition, a comparison with the existing verification approaches for PLC programs\nis discussed.
Loading....